(TML)

  %We now prove several little theorems which will
   later be set up as simprules.
  %

let g = "NULL UU == UU";;
let gl, proof = SIMPTAC (g,ssadd defNULL BASICSS,[]);;
let NULLUUthm = proof[];;
hyp(NULLUUthm);;

let g = "NULL NIL == TT";;
let gl,proof = SIMPTAC (g,itlist ssadd [defNULL;defNIL] BASICSS,[]);;
let NULLNILthm = proof [];;
hyp(NULLNILthm);;

let g = "NULL(CONS A L) == FF";;
let gl,proof = SIMPTAC (g,itlist ssadd [defNULL;defCONS] BASICSS,[]);;
let NULLCONSthm = proof[];;
hyp(NULLCONSthm);;